T:Type, P:((T List)T).
(L:(T List), x:T. Dec(P(L,x)))
 (L:(T List). Dec(L':T List. x:T. (L = (L' @ [x]) & P(L',x)))) 

latex

Definitions	t  T, x:A. B(x), P  Q, Dec(P), , x(s1,s2), P & Q, x:A. B(x), P  Q, null(as), b, False, as @ bs, A, {T}, P  Q, last(L), ||as||, firstn(n;as), Top, S  T, i  j , A  B, i  j < k, {i..j}, SQType(T), True, T, P  Q, hd(l), i <z j, i z j, l[i], tl(l), b, if b then t else f fi , nth_tl(n;as), Y
Lemmas	assert of null, last append, false wf, length append, squash wf, true wf, firstn wf, firstn append, non neg length, length wf1, firstn length, top wf, last wf, not wf, last lemma, append is nil, decidable false, append wf, decidable wf, decidable assert, null wf